type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
type exposeVersionType;
var $Heap : <x>[ref, name]x where IsHeap($Heap);
function IsHeap(h : <x>[ref, name]x) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $localinv : name;
const $exposeVersion : name;
axiom (DeclType($exposeVersion) == System.Object);
const $sharingMode : name;
const $SharingMode_Unshared : name;
const $SharingMode_LockProtected : name;
const $ownerRef : name;
const $ownerFrame : name;
const $PeerGroupPlaceholder : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: {ClassRepr(c0), ClassRepr(c1)} ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall T : name, h : <x>[ref, name]x :: {h[ClassRepr(T), $ownerFrame]} (IsHeap(h) ==> (h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder)));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($localinv);
axiom !IsDirectlyModifiableField($ownerRef);
axiom !IsDirectlyModifiableField($ownerFrame);
axiom !IsDirectlyModifiableField($exposeVersion);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($localinv);
axiom !IsStaticField($exposeVersion);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: {ArrayIndex(a, d, x, y), ArrayIndex(a, d, x', y')} ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: RefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: RefArray(T, r))) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: NonNullRefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: NonNullRefArray(T, r))) ==> $IsNotNull(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: RefArray(T, r))} (((a != null) && ($typeof(a) <: RefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: NonNullRefArray(T, r))} (((a != null) && ($typeof(a) <: NonNullRefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: ValueArray(T, r))} (((a != null) && ($typeof(a) <: ValueArray(T, r))) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: {$DimLength(a, 0)} (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const $ArrayCategoryValue : name;
const $ArrayCategoryRef : name;
const $ArrayCategoryNonNullRef : name;
function $ArrayCategory(arrayType : name) returns (arrayCategory : name);
axiom (forall T : name, ET : name, r : int :: {(T <: ValueArray(ET, r))} ((T <: ValueArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryValue)));
axiom (forall T : name, ET : name, r : int :: {(T <: RefArray(ET, r))} ((T <: RefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryRef)));
axiom (forall T : name, ET : name, r : int :: {(T <: NonNullRefArray(ET, r))} ((T <: NonNullRefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryNonNullRef)));
const System.Array : name;
axiom (System.Array <: System.Object);
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
function NonNullRefArray(elementType : name, rank : int) returns ($$unnamed~ak : name);
axiom (forall T : name, r : int :: {NonNullRefArray(T, r)} (NonNullRefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (NonNullRefArray(U, r) <: NonNullRefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(NonNullRefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: NonNullRefArray(A, r))} ((T <: NonNullRefArray(A, r)) ==> ((T == NonNullRefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((NonNullRefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == NonNullRefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~al : name);
function $StructGet<any>($$unnamed~an : struct, $$unnamed~am : name) returns ($$unnamed~ao : any);
function $StructSet<any>($$unnamed~ar : struct, $$unnamed~aq : name, $$unnamed~ap : any) returns ($$unnamed~as : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~at : bool);
function $typeof($$unnamed~au : ref) returns ($$unnamed~av : name);
function $BaseClass(sub : name) returns (base : name);
function AsDirectSubClass(sub : name, base : name) returns (sub' : name);
function OneClassDown(sub : name, base : name) returns (directSub : name);
axiom (forall A : name, B : name, C : name :: {(C <: AsDirectSubClass(B, A))} ((C <: AsDirectSubClass(B, A)) ==> (OneClassDown(C, A) == B)));
function $IsValueType($$unnamed~aw : name) returns ($$unnamed~ax : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
const System.Object : name;
function $IsTokenForType($$unnamed~az : struct, $$unnamed~ay : name) returns ($$unnamed~ba : bool);
function TypeObject($$unnamed~bb : name) returns ($$unnamed~bc : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function TypeName($$unnamed~bd : ref) returns ($$unnamed~be : name);
axiom (forall T : name :: {TypeObject(T)} (TypeName(TypeObject(T)) == T));
function $Is($$unnamed~bg : ref, $$unnamed~bf : name) returns ($$unnamed~bh : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall h : <x>[ref, name]x, o : ref :: {($typeof(o) <: System.Array), h[o, $inv]} (((IsHeap(h) && (o != null)) && ($typeof(o) <: System.Array)) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
function IsAllocated<any>(h : <x>[ref, name]x, o : any) returns ($$unnamed~bo : bool);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {IsAllocated(h, h[o, f])} ((IsHeap(h) && h[o, $allocated]) ==> IsAllocated(h, h[o, f])));
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[h[o, f], $allocated]} ((IsHeap(h) && h[o, $allocated]) ==> h[h[o, f], $allocated]));
axiom (forall h : <x>[ref, name]x, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, ValueArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall h : <x>[ref, name]x, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
const $BeingConstructed : ref;
const $NonNullFieldsAreInitialized : name;
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (((IsHeap(h) && (o != null)) && ((o != $BeingConstructed) || (h[$BeingConstructed, $NonNullFieldsAreInitialized] == true))) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function $IsMemberlessType($$unnamed~bp : name) returns ($$unnamed~bq : bool);
axiom (forall o : ref :: {$IsMemberlessType($typeof(o))} !$IsMemberlessType($typeof(o)));
function $IsImmutable(T : name) returns ($$unnamed~br : bool);
axiom !$IsImmutable(System.Object);
function $AsImmutable(T : name) returns (theType : name);
function $AsMutable(T : name) returns (theType : name);
axiom (forall T : name, U : name :: {(U <: $AsImmutable(T))} ((U <: $AsImmutable(T)) ==> ($IsImmutable(U) && ($AsImmutable(U) == U))));
axiom (forall T : name, U : name :: {(U <: $AsMutable(T))} ((U <: $AsMutable(T)) ==> (!$IsImmutable(U) && ($AsMutable(U) == U))));
function AsOwner(string : ref, owner : ref) returns (theString : ref);
axiom (forall o : ref, T : name :: {($typeof(o) <: $AsImmutable(T))} ((((o != null) && (o != $BeingConstructed)) && ($typeof(o) <: $AsImmutable(T))) ==> (forall h : <x>[ref, name]x :: {IsHeap(h)} (IsHeap(h) ==> (((((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o))) && (h[o, $ownerFrame] == $PeerGroupPlaceholder)) && (AsOwner(o, h[o, $ownerRef]) == o)) && (forall t : ref :: {AsOwner(o, h[t, $ownerRef])} ((AsOwner(o, h[t, $ownerRef]) == o) ==> ((t == o) || (h[t, $ownerFrame] != $PeerGroupPlaceholder)))))))));
const System.String : name;
function $StringLength($$unnamed~bs : ref) returns ($$unnamed~bt : int);
axiom (forall s : ref :: {$StringLength(s)} (0 <= $StringLength(s)));
function AsRepField(f : name, declaringType : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRepField(f, T)]} ((IsHeap(h) && (h[o, AsRepField(f, T)] != null)) ==> ((h[h[o, AsRepField(f, T)], $ownerRef] == o) && (h[h[o, AsRepField(f, T)], $ownerFrame] == T))));
function AsPeerField(f : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[o, AsPeerField(f)]} ((IsHeap(h) && (h[o, AsPeerField(f)] != null)) ==> ((h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef]) && (h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]))));
axiom (forall h : <x>[ref, name]x, o : ref :: {(h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])} ((((IsHeap(h) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
procedure $SetOwner(o : ref, ow : ref, fr : name);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[o, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[o, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == ow) && ($Heap[p, $ownerFrame] == fr))));
  

procedure $UpdateOwnersForRep(o : ref, T : name, e : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[e, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((e == null) ==> ($Heap == old($Heap)));
  ensures ((e != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[e, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == o) && ($Heap[p, $ownerFrame] == T)))));
  

procedure $UpdateOwnersForPeer(c : ref, d : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} ((((F != $ownerRef) && (F != $ownerFrame)) || old(((($Heap[p, $ownerRef] != $Heap[c, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[c, $ownerFrame])) && (($Heap[p, $ownerRef] != $Heap[d, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]))))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((d == null) ==> ($Heap == old($Heap)));
  ensures ((d != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} (((old(($Heap[p, $ownerRef] == $Heap[c, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[c, $ownerFrame]))) || (old(($Heap[p, $ownerRef] == $Heap[d, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[d, $ownerFrame])))) ==> ((((old($Heap)[d, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[c, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame])) || (((old($Heap)[d, $ownerFrame] != $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[d, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[d, $ownerFrame]))))));
  

const $FirstConsistentOwner : name;
function $AsPureObject($$unnamed~bu : ref) returns ($$unnamed~bv : ref);
function ##FieldDependsOnFCO<any>(o : ref, f : name, ev : exposeVersionType) returns (value : any);
axiom (forall o : ref, f : name, h : <x>[ref, name]x :: {h[$AsPureObject(o), f]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion]))));
axiom (forall o : ref, h : <x>[ref, name]x :: {h[o, $FirstConsistentOwner]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (((h[o, $FirstConsistentOwner] != null) && (h[h[o, $FirstConsistentOwner], $allocated] == true)) && (((h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder) || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame])) || (h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))))));
function Box<any>($$unnamed~bx : any, $$unnamed~bw : ref) returns ($$unnamed~by : ref);
function Unbox<any>($$unnamed~bz : ref) returns ($$unnamed~ca : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
function UnboxedType($$unnamed~cb : ref) returns ($$unnamed~cc : name);
axiom (forall p : ref :: {$IsValueType(UnboxedType(p))} ($IsValueType(UnboxedType(p)) ==> (forall<any> heap : <x>[ref, name]x, x : any :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> ((heap[Box(x, p), $inv] == $typeof(Box(x, p))) && (heap[Box(x, p), $localinv] == $typeof(Box(x, p))))))));
axiom (forall<any> x : any, p : ref :: {(UnboxedType(Box(x, p)) <: System.Object)} (((UnboxedType(Box(x, p)) <: System.Object) && (Box(x, p) == p)) ==> (x == p)));
function BoxTester(p : ref, typ : name) returns ($$unnamed~cd : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.SByte : name;
axiom $IsValueType(System.SByte);
const System.Byte : name;
axiom $IsValueType(System.Byte);
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.UInt16 : name;
axiom $IsValueType(System.UInt16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.UInt32 : name;
axiom $IsValueType(System.UInt32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.UInt64 : name;
axiom $IsValueType(System.UInt64);
const System.Char : name;
axiom $IsValueType(System.Char);
const int#m2147483648 : int;
const int#2147483647 : int;
const int#4294967295 : int;
const int#m9223372036854775808 : int;
const int#9223372036854775807 : int;
const int#18446744073709551615 : int;
axiom (int#m9223372036854775808 < int#m2147483648);
axiom (int#m2147483648 < (0 - 100000));
axiom (100000 < int#2147483647);
axiom (int#2147483647 < int#4294967295);
axiom (int#4294967295 < int#9223372036854775807);
axiom (int#9223372036854775807 < int#18446744073709551615);
function InRange(i : int, T : name) returns ($$unnamed~ce : bool);
axiom (forall i : int :: (InRange(i, System.SByte) <==> (((0 - 128) <= i) && (i < 128))));
axiom (forall i : int :: (InRange(i, System.Byte) <==> ((0 <= i) && (i < 256))));
axiom (forall i : int :: (InRange(i, System.Int16) <==> (((0 - 32768) <= i) && (i < 32768))));
axiom (forall i : int :: (InRange(i, System.UInt16) <==> ((0 <= i) && (i < 65536))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((int#m2147483648 <= i) && (i <= int#2147483647))));
axiom (forall i : int :: (InRange(i, System.UInt32) <==> ((0 <= i) && (i <= int#4294967295))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((int#m9223372036854775808 <= i) && (i <= int#9223372036854775807))));
axiom (forall i : int :: (InRange(i, System.UInt64) <==> ((0 <= i) && (i <= int#18446744073709551615))));
axiom (forall i : int :: (InRange(i, System.Char) <==> ((0 <= i) && (i < 65536))));
function $IntToInt(val : int, fromType : name, toType : name) returns ($$unnamed~cf : int);
function $IntToReal($$unnamed~cg : int, fromType : name, toType : name) returns ($$unnamed~ch : real);
function $RealToInt($$unnamed~ci : real, fromType : name, toType : name) returns ($$unnamed~cj : int);
function $RealToReal(val : real, fromType : name, toType : name) returns ($$unnamed~ck : real);
function $SizeIs($$unnamed~cm : name, $$unnamed~cl : int) returns ($$unnamed~cn : bool);
function $IfThenElse<any>($$unnamed~cq : bool, $$unnamed~cp : any, $$unnamed~co : any) returns ($$unnamed~cr : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cs : int) returns ($$unnamed~ct : int);
function #and($$unnamed~cv : int, $$unnamed~cu : int) returns ($$unnamed~cw : int);
function #or($$unnamed~cy : int, $$unnamed~cx : int) returns ($$unnamed~cz : int);
function #xor($$unnamed~db : int, $$unnamed~da : int) returns ($$unnamed~dc : int);
function #shl($$unnamed~de : int, $$unnamed~dd : int) returns ($$unnamed~df : int);
function #shr($$unnamed~dh : int, $$unnamed~dg : int) returns ($$unnamed~di : int);
function #rneg($$unnamed~dj : real) returns ($$unnamed~dk : real);
function #radd($$unnamed~dm : real, $$unnamed~dl : real) returns ($$unnamed~dn : real);
function #rsub($$unnamed~dp : real, $$unnamed~do : real) returns ($$unnamed~dq : real);
function #rmul($$unnamed~ds : real, $$unnamed~dr : real) returns ($$unnamed~dt : real);
function #rdiv($$unnamed~dv : real, $$unnamed~du : real) returns ($$unnamed~dw : real);
function #rmod($$unnamed~dy : real, $$unnamed~dx : real) returns ($$unnamed~dz : real);
function #rLess($$unnamed~eb : real, $$unnamed~ea : real) returns ($$unnamed~ec : bool);
function #rAtmost($$unnamed~ee : real, $$unnamed~ed : real) returns ($$unnamed~ef : bool);
function #rEq($$unnamed~eh : real, $$unnamed~eg : real) returns ($$unnamed~ei : bool);
function #rNeq($$unnamed~ek : real, $$unnamed~ej : real) returns ($$unnamed~el : bool);
function #rAtleast($$unnamed~en : real, $$unnamed~em : real) returns ($$unnamed~eo : bool);
function #rGreater($$unnamed~eq : real, $$unnamed~ep : real) returns ($$unnamed~er : bool);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall x : int, y : int :: {((x - y) % y)} (((0 <= (x - y)) && (0 <= y)) ==> (((x - y) % y) == (x % y))));
axiom (forall a : int, b : int, d : int :: {(a % d), (b % d)} ((((2 <= d) && ((a % d) == (b % d))) && (a < b)) ==> ((a + d) <= b)));
axiom (forall x : int, y : int :: {#and(x, y)} (((0 <= x) || (0 <= y)) ==> (0 <= #and(x, y))));
axiom (forall x : int, y : int :: {#or(x, y)} (((0 <= x) && (0 <= y)) ==> ((0 <= #or(x, y)) && (#or(x, y) <= (x + y)))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
function #System.String.IsInterned$System.String$notnull($$unnamed~es : ref) returns ($$unnamed~et : ref);
function #System.String.Equals$System.String($$unnamed~ev : ref, $$unnamed~eu : ref) returns ($$unnamed~ew : bool);
function #System.String.Equals$System.String$System.String($$unnamed~ey : ref, $$unnamed~ex : ref) returns ($$unnamed~ez : bool);
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String(a, b)} (#System.String.Equals$System.String(a, b) == #System.String.Equals$System.String$System.String(a, b)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} (#System.String.Equals$System.String$System.String(a, b) == #System.String.Equals$System.String$System.String(b, a)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} ((((a != null) && (b != null)) && #System.String.Equals$System.String$System.String(a, b)) ==> (#System.String.IsInterned$System.String$notnull(a) == #System.String.IsInterned$System.String$notnull(b))));
const $UnknownRef : ref;
const A.y : name;
const B.others : name;
const AbstractCity0.a0 : name;
const C.others : name;
const A.x : name;
const A.others : name;
const AnotherInvariantNameIssue.x : name;
const A.z : name;
const AbstractCity1.a1 : name;
const System.Runtime.InteropServices._Exception : name;
const AbstractCity1 : name;
const Microsoft.Contracts.GuardException : name;
const B : name;
const System.Boolean : name;
const Microsoft.Contracts.ICheckedException : name;
const AbstractCity0 : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const System.Reflection.MemberInfo : name;
const System.Runtime.Serialization.ISerializable : name;
const A : name;
const System.Reflection.IReflect : name;
const System.Runtime.InteropServices._MemberInfo : name;
const System.Exception : name;
const System.Runtime.InteropServices._Type : name;
const C : name;
const AnotherInvariantNameIssue : name;
const System.Reflection.ICustomAttributeProvider : name;
axiom !IsStaticField(A.others);
axiom IsDirectlyModifiableField(A.others);
axiom (AsRepField(A.others, A) == A.others);
axiom (DeclType(A.others) == A);
axiom (AsNonNullRefField(A.others, RefArray(A, 1)) == A.others);
axiom !IsStaticField(A.x);
axiom IsDirectlyModifiableField(A.x);
axiom (DeclType(A.x) == A);
axiom (AsRangeField(A.x, System.Int32) == A.x);
axiom !IsStaticField(A.y);
axiom IsDirectlyModifiableField(A.y);
axiom (DeclType(A.y) == A);
axiom (AsRangeField(A.y, System.Int32) == A.y);
axiom !IsStaticField(A.z);
axiom IsDirectlyModifiableField(A.z);
axiom (DeclType(A.z) == A);
axiom (AsRangeField(A.z, System.Int32) == A.z);
axiom !IsStaticField(AbstractCity0.a0);
axiom IsDirectlyModifiableField(AbstractCity0.a0);
axiom (DeclType(AbstractCity0.a0) == AbstractCity0);
axiom (AsRefField(AbstractCity0.a0, A) == AbstractCity0.a0);
axiom !IsStaticField(B.others);
axiom IsDirectlyModifiableField(B.others);
axiom (AsRepField(B.others, B) == B.others);
axiom (DeclType(B.others) == B);
axiom (AsNonNullRefField(B.others, RefArray(System.Object, 1)) == B.others);
axiom !IsStaticField(AbstractCity1.a1);
axiom IsDirectlyModifiableField(AbstractCity1.a1);
axiom (DeclType(AbstractCity1.a1) == AbstractCity1);
axiom (AsRefField(AbstractCity1.a1, A) == AbstractCity1.a1);
axiom !IsStaticField(C.others);
axiom IsDirectlyModifiableField(C.others);
axiom (AsRepField(C.others, C) == C.others);
axiom (DeclType(C.others) == C);
axiom (AsNonNullRefField(C.others, RefArray(System.Object, 1)) == C.others);
axiom !IsStaticField(AnotherInvariantNameIssue.x);
axiom IsDirectlyModifiableField(AnotherInvariantNameIssue.x);
axiom (DeclType(AnotherInvariantNameIssue.x) == AnotherInvariantNameIssue);
axiom (AsRangeField(AnotherInvariantNameIssue.x, System.Int32) == AnotherInvariantNameIssue.x);
axiom (A <: A);
axiom ($BaseClass(A) == System.Object);
axiom ((A <: $BaseClass(A)) && (AsDirectSubClass(A, $BaseClass(A)) == A));
axiom (!$IsImmutable(A) && ($AsMutable(A) == A));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: A)} (((IsHeap($h) && ($h[$oi, $inv] <: A)) && ($h[$oi, $localinv] != System.Object)) ==> (forall ^ijk : int :: (((0 <= ^ijk) && (^ijk <= ($Length($h[$oi, A.others]) - 1))) ==> (((^ijk % 2) == 0) ==> ((RefArrayGet($h[$h[$oi, A.others], $elements], ^ijk) != null) ==> ($h[RefArrayGet($h[$h[$oi, A.others], $elements], ^ijk), A.x] == 7)))))));
axiom (forall $U : name :: {($U <: System.Boolean)} (($U <: System.Boolean) ==> ($U == System.Boolean)));
procedure A.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation A.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var local0 : bool where true;
  var local1 : int where InRange(local1, System.Int32);
  var stack0o : ref;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local2 : bool where true;
  var stack1o : ref;
  var SS$Display.Return.Local : bool where true;
  var stack50000o : ref;
  var $Heap$block3094$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, A); goto $$entry~b;
  $$entry~b: assume ($Heap[this, $allocated] == true); goto $$entry~a;
  $$entry~a: throwException := throwException$in; goto block3060;
  block3060: goto block3077;
  block3077: local0 := true; goto $$block3077~a;
  $$block3077~a: local1 := 0; goto block3094$LoopPreheader;
  block3094: assume (((forall $o : ref :: (($Heap$block3094$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block3094$LoopPreheader[$ot, $allocated] == true) && ($Heap$block3094$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block3094$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block3094$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block3094$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block3094~i;
  $$block3094~i: assume (forall $o : ref :: ((($Heap$block3094$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block3094$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block3094$LoopPreheader[$o, $allocated] != true))); goto $$block3094~h;
  $$block3094~h: assume (forall $o : ref :: ((($Heap$block3094$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block3094~g;
  $$block3094~g: assert (forall $o : ref :: ((($o != null) && ($Heap$block3094$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block3094$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block3094$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block3094~f;
  $$block3094~f: assert (this != null); goto $$block3094~e;
  $$block3094~e: stack0o := $Heap[this, A.others]; goto $$block3094~d;
  $$block3094~d: assert (stack0o != null); goto $$block3094~c;
  $$block3094~c: stack0i := $Length(stack0o); goto $$block3094~b;
  $$block3094~b: stack1i := 1; goto $$block3094~a;
  $$block3094~a: stack0i := (stack0i - stack1i); goto true3094to3298, false3094to3111;
  true3094to3298: assume (local1 > stack0i); goto block3298;
  false3094to3111: assume (local1 <= stack0i); goto block3111;
  block3298: goto true3298to3400, false3298to3315;
  block3111: stack0i := 2; goto $$block3111~c;
  $$block3111~c: assert (stack0i != 0); goto $$block3111~b;
  $$block3111~b: stack0i := (local1 % stack0i); goto $$block3111~a;
  $$block3111~a: stack1i := 0; goto true3111to3247, false3111to3128;
  true3298to3400: assume local0; goto block3400;
  false3298to3315: assume !local0; goto block3315;
  block3400: local2 := true; goto block3417;
  block3315: stack0b := throwException; goto true3315to3366, false3315to3332;
  true3111to3247: assume (stack0i != stack1i); goto block3247;
  false3111to3128: assume (stack0i == stack1i); goto block3128;
  block3247: goto true3247to3281, false3247to3264;
  block3128: assert (this != null); goto $$block3128~g;
  $$block3128~g: stack0o := $Heap[this, A.others]; goto $$block3128~f;
  $$block3128~f: stack1i := local1; goto $$block3128~e;
  $$block3128~e: assert (stack0o != null); goto $$block3128~d;
  $$block3128~d: assert (0 <= stack1i); goto $$block3128~c;
  $$block3128~c: assert (stack1i < $Length(stack0o)); goto $$block3128~b;
  $$block3128~b: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block3128~a;
  $$block3128~a: stack1o := null; goto true3128to3213, false3128to3145;
  true3315to3366: assume !stack0b; goto block3366;
  false3315to3332: assume stack0b; goto block3332;
  block3366: local2 := false; goto block3417;
  block3332: assume false; goto $$block3332~i;
  $$block3332~i: havoc stack50000o; goto $$block3332~h;
  $$block3332~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block3332~g;
  $$block3332~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block3332~f;
  $$block3332~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block3332~e;
  $$block3332~e: assert (stack50000o != null); goto $$block3332~d;
  $$block3332~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block3332~c;
  $$block3332~c: stack0o := stack50000o; goto $$block3332~b;
  $$block3332~b: assert (stack0o != null); goto $$block3332~a;
  $$block3332~a: assume false; return;
  true3247to3281: assume local0; goto block3281;
  false3247to3264: assume !local0; goto block3264;
  block3281: stack0i := 1; goto $$block3281~b;
  $$block3281~b: stack0i := (local1 + stack0i); goto $$block3281~a;
  $$block3281~a: local1 := stack0i; goto block3094;
  block3264: goto block3298;
  true3128to3213: assume (stack0o == stack1o); goto block3213;
  false3128to3145: assume (stack0o != stack1o); goto block3145;
  block3213: stack0b := true; goto block3230;
  block3145: assert (this != null); goto $$block3145~i;
  $$block3145~i: stack0o := $Heap[this, A.others]; goto $$block3145~h;
  $$block3145~h: stack1i := local1; goto $$block3145~g;
  $$block3145~g: assert (stack0o != null); goto $$block3145~f;
  $$block3145~f: assert (0 <= stack1i); goto $$block3145~e;
  $$block3145~e: assert (stack1i < $Length(stack0o)); goto $$block3145~d;
  $$block3145~d: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block3145~c;
  $$block3145~c: assert (stack0o != null); goto $$block3145~b;
  $$block3145~b: stack0i := $Heap[stack0o, A.x]; goto $$block3145~a;
  $$block3145~a: stack1i := 7; goto true3145to3179, false3145to3162;
  block3417: SS$Display.Return.Local := local2; goto $$block3417~b;
  $$block3417~b: stack0b := local2; goto $$block3417~a;
  $$block3417~a: $result := stack0b; return;
  true3145to3179: assume (stack0i == stack1i); goto block3179;
  false3145to3162: assume (stack0i != stack1i); goto block3162;
  block3179: stack0b := true; goto block3196;
  block3162: stack0b := false; goto block3196;
  block3230: local0 := stack0b; goto block3247;
  block3196: goto block3230;
  block3094$LoopPreheader: $Heap$block3094$LoopPreheader := $Heap; goto block3094;
  
}

axiom (Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException);
axiom (Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException);
axiom (System.Exception <: System.Exception);
axiom ($BaseClass(System.Exception) == System.Object);
axiom ((System.Exception <: $BaseClass(System.Exception)) && (AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception));
axiom (!$IsImmutable(System.Exception) && ($AsMutable(System.Exception) == System.Exception));
axiom (System.Runtime.Serialization.ISerializable <: System.Object);
axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable);
axiom (System.Exception <: System.Runtime.Serialization.ISerializable);
axiom (System.Runtime.InteropServices._Exception <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Exception);
axiom (System.Exception <: System.Runtime.InteropServices._Exception);
axiom ($BaseClass(Microsoft.Contracts.GuardException) == System.Exception);
axiom ((Microsoft.Contracts.GuardException <: $BaseClass(Microsoft.Contracts.GuardException)) && (AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException));
axiom (!$IsImmutable(Microsoft.Contracts.GuardException) && ($AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException));
axiom ($BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom ((Microsoft.Contracts.ObjectInvariantException <: $BaseClass(Microsoft.Contracts.ObjectInvariantException)) && (AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException));
axiom (!$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && ($AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Microsoft.Contracts.ObjectInvariantException <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure A..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == A)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(A <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation A..ctor(this : ref) {
  var stack0i : int;
  var stack0o : ref;
  var temp0 : ref;
  entry: assume $IsNotNull(this, A); goto $$entry~g;
  $$entry~g: assume ($Heap[this, $allocated] == true); goto $$entry~f;
  $$entry~f: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~e;
  $$entry~e: assume ($Heap[this, A.x] == 0); goto $$entry~d;
  $$entry~d: assume ($Heap[this, A.y] == 0); goto $$entry~c;
  $$entry~c: assume ($Heap[this, A.z] == 0); goto block4505;
  block4505: goto block4522;
  block4522: assert (this != null); goto $$block4522~a;
  $$block4522~a: call System.Object..ctor(this); goto block4590;
  block4590: stack0i := 10; goto $$block4590~v;
  $$block4590~v: assert (0 <= stack0i); goto $$block4590~u;
  $$block4590~u: havoc stack0o; goto $$block4590~t;
  $$block4590~t: assume (($Heap[stack0o, $allocated] == false) && ($Length(stack0o) == stack0i)); goto $$block4590~s;
  $$block4590~s: assume $IsNotNull(stack0o, RefArray(A, 1)); goto $$block4590~r;
  $$block4590~r: assume (($Heap[stack0o, $ownerRef] == stack0o) && ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block4590~q;
  $$block4590~q: assume ((($Heap[stack0o, $inv] == RefArray(A, 1)) && ($Heap[stack0o, $localinv] == RefArray(A, 1))) && ((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame])))); goto $$block4590~p;
  $$block4590~p: assume (forall $i : int :: (RefArrayGet($Heap[stack0o, $elements], $i) == null)); goto $$block4590~o;
  $$block4590~o: $Heap := $Heap[stack0o, $allocated := true]; goto $$block4590~n;
  $$block4590~n: assume IsHeap($Heap); goto $$block4590~m;
  $$block4590~m: assert (this != null); goto $$block4590~l;
  $$block4590~l: assert (!($Heap[this, $inv] <: A) || ($Heap[this, $localinv] == System.Object)); goto $$block4590~k;
  $$block4590~k: assert (($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || (($Heap[stack0o, $ownerRef] == this) && ($Heap[stack0o, $ownerFrame] == A))); goto $$block4590~j;
  $$block4590~j: $Heap := $Heap[this, A.others := stack0o]; goto $$block4590~i;
  $$block4590~i: call $UpdateOwnersForRep(this, A, stack0o); goto $$block4590~h;
  $$block4590~h: assume IsHeap($Heap); goto $$block4590~g;
  $$block4590~g: temp0 := this; goto $$block4590~f;
  $$block4590~f: assert (temp0 != null); goto $$block4590~e;
  $$block4590~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block4590~d;
  $$block4590~d: assert (forall ^ijk : int :: (((0 <= ^ijk) && (^ijk <= ($Length($Heap[temp0, A.others]) - 1))) ==> (((^ijk % 2) == 0) ==> ((RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk) != null) ==> ($Heap[RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk), A.x] == 7))))); goto $$block4590~c;
  $$block4590~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == A)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block4590~b;
  $$block4590~b: $Heap := $Heap[temp0, $inv := A]; goto $$block4590~a;
  $$block4590~a: assume IsHeap($Heap); return;
  
}

procedure System.Object..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(System.Object <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure A.M(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation A.M(this : ref) {
  var ijk : int where InRange(ijk, System.Int32);
  var local2 : int where InRange(local2, System.Int32);
  var stack0i : int;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var local5 : int where InRange(local5, System.Int32);
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, A); goto $$entry~h;
  $$entry~h: assume ($Heap[this, $allocated] == true); goto block5457;
  block5457: goto block5610;
  block5610: ijk := 0; goto $$block5610~p;
  $$block5610~p: local2 := ijk; goto $$block5610~o;
  $$block5610~o: stack0i := 1; goto $$block5610~n;
  $$block5610~n: stack0i := (local2 + stack0i); goto $$block5610~m;
  $$block5610~m: ijk := stack0i; goto $$block5610~l;
  $$block5610~l: stack0i := local2; goto $$block5610~k;
  $$block5610~k: temp0 := this; goto $$block5610~j;
  $$block5610~j: havoc stack1s; goto $$block5610~i;
  $$block5610~i: assume $IsTokenForType(stack1s, A); goto $$block5610~h;
  $$block5610~h: stack1o := TypeObject(A); goto $$block5610~g;
  $$block5610~g: assert (temp0 != null); goto $$block5610~f;
  $$block5610~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: A)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block5610~e;
  $$block5610~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block5610~d;
  $$block5610~d: havoc temp1; goto $$block5610~c;
  $$block5610~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block5610~b;
  $$block5610~b: assume IsHeap($Heap); goto $$block5610~a;
  $$block5610~a: local4 := null; goto block5627;
  block5627: assert (this != null); goto $$block5627~i;
  $$block5627~i: local5 := $Heap[this, A.x]; goto $$block5627~h;
  $$block5627~h: stack0i := 1; goto $$block5627~g;
  $$block5627~g: stack0i := (local5 + stack0i); goto $$block5627~f;
  $$block5627~f: assert (this != null); goto $$block5627~e;
  $$block5627~e: assert (!($Heap[this, $inv] <: A) || ($Heap[this, $localinv] == System.Object)); goto $$block5627~d;
  $$block5627~d: assert (forall $o : ref, ^ijk : int :: (((0 <= ^ijk) && (^ijk <= ($Length($Heap[this, A.others]) - 1))) ==> (((^ijk % 2) == 0) ==> ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: A)) && (RefArrayGet($Heap[$Heap[$o, A.others], $elements], ^ijk) == this)) ==> (!($Heap[$o, $inv] <: A) || ($Heap[$o, $localinv] == System.Object)))))); goto $$block5627~c;
  $$block5627~c: $Heap := $Heap[this, A.x := stack0i]; goto $$block5627~b;
  $$block5627~b: assume IsHeap($Heap); goto $$block5627~a;
  $$block5627~a: stack0i := local5; goto block5712;
  block5712: stack0o := null; goto true5712to5780, false5712to5729;
  true5712to5780: assume (local4 == stack0o); goto block5780;
  false5712to5729: assume (local4 != stack0o); goto block5729;
  block5780: havoc stack0s; goto $$block5780~h;
  $$block5780~h: assume $IsTokenForType(stack0s, A); goto $$block5780~g;
  $$block5780~g: stack0o := TypeObject(A); goto $$block5780~f;
  $$block5780~f: assert (temp0 != null); goto $$block5780~e;
  $$block5780~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block5780~d;
  $$block5780~d: assert (forall ^ijk : int :: (((0 <= ^ijk) && (^ijk <= ($Length($Heap[temp0, A.others]) - 1))) ==> (((^ijk % 2) == 0) ==> ((RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk) != null) ==> ($Heap[RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk), A.x] == 7))))); goto $$block5780~c;
  $$block5780~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == A)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block5780~b;
  $$block5780~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block5780~a;
  $$block5780~a: assume IsHeap($Heap); goto block5763;
  block5729: goto true5729to5780, false5729to5746;
  true5729to5780: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block5780;
  false5729to5746: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block5746;
  block5746: goto block5763;
  block5763: goto block5678;
  block5678: return;
  
}

axiom (System.Type <: System.Type);
axiom (System.Reflection.MemberInfo <: System.Reflection.MemberInfo);
axiom ($BaseClass(System.Reflection.MemberInfo) == System.Object);
axiom ((System.Reflection.MemberInfo <: $BaseClass(System.Reflection.MemberInfo)) && (AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo));
axiom ($IsImmutable(System.Reflection.MemberInfo) && ($AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo));
axiom (System.Reflection.ICustomAttributeProvider <: System.Object);
axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider);
axiom (System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider);
axiom (System.Runtime.InteropServices._MemberInfo <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo);
axiom (System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo);
axiom $IsMemberlessType(System.Reflection.MemberInfo);
axiom ($BaseClass(System.Type) == System.Reflection.MemberInfo);
axiom ((System.Type <: $BaseClass(System.Type)) && (AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type));
axiom ($IsImmutable(System.Type) && ($AsImmutable(System.Type) == System.Type));
axiom (System.Runtime.InteropServices._Type <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Type);
axiom (System.Type <: System.Runtime.InteropServices._Type);
axiom (System.Reflection.IReflect <: System.Object);
axiom $IsMemberlessType(System.Reflection.IReflect);
axiom (System.Type <: System.Reflection.IReflect);
axiom $IsMemberlessType(System.Type);
axiom (Microsoft.Contracts.ICheckedException <: System.Object);
axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException);
procedure A.N(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation A.N(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, A); goto $$entry~i;
  $$entry~i: assume ($Heap[this, $allocated] == true); goto block6987;
  block6987: goto block7140;
  block7140: temp0 := this; goto $$block7140~j;
  $$block7140~j: havoc stack1s; goto $$block7140~i;
  $$block7140~i: assume $IsTokenForType(stack1s, A); goto $$block7140~h;
  $$block7140~h: stack1o := TypeObject(A); goto $$block7140~g;
  $$block7140~g: assert (temp0 != null); goto $$block7140~f;
  $$block7140~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: A)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block7140~e;
  $$block7140~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block7140~d;
  $$block7140~d: havoc temp1; goto $$block7140~c;
  $$block7140~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block7140~b;
  $$block7140~b: assume IsHeap($Heap); goto $$block7140~a;
  $$block7140~a: local2 := null; goto block7157;
  block7157: assert (this != null); goto $$block7157~i;
  $$block7157~i: local3 := $Heap[this, A.y]; goto $$block7157~h;
  $$block7157~h: stack0i := 1; goto $$block7157~g;
  $$block7157~g: stack0i := (local3 + stack0i); goto $$block7157~f;
  $$block7157~f: assert (this != null); goto $$block7157~e;
  $$block7157~e: assert (!($Heap[this, $inv] <: A) || ($Heap[this, $localinv] == System.Object)); goto $$block7157~d;
  $$block7157~d: assert (forall $o : ref, ^i : int :: (((0 <= ^i) && (^i <= ($Length($Heap[this, B.others]) - 1))) ==> ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: B)) && ($Heap[RefArrayGet($Heap[$Heap[$o, B.others], $elements], ^i), AbstractCity0.a0] == this)) ==> (!($Heap[$o, $inv] <: B) || ($Heap[$o, $localinv] == System.Object))))); goto $$block7157~c;
  $$block7157~c: $Heap := $Heap[this, A.y := stack0i]; goto $$block7157~b;
  $$block7157~b: assume IsHeap($Heap); goto $$block7157~a;
  $$block7157~a: stack0i := local3; goto block7242;
  block7242: stack0o := null; goto true7242to7310, false7242to7259;
  true7242to7310: assume (local2 == stack0o); goto block7310;
  false7242to7259: assume (local2 != stack0o); goto block7259;
  block7310: havoc stack0s; goto $$block7310~h;
  $$block7310~h: assume $IsTokenForType(stack0s, A); goto $$block7310~g;
  $$block7310~g: stack0o := TypeObject(A); goto $$block7310~f;
  $$block7310~f: assert (temp0 != null); goto $$block7310~e;
  $$block7310~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block7310~d;
  $$block7310~d: assert (forall ^ijk : int :: (((0 <= ^ijk) && (^ijk <= ($Length($Heap[temp0, A.others]) - 1))) ==> (((^ijk % 2) == 0) ==> ((RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk) != null) ==> ($Heap[RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk), A.x] == 7))))); goto $$block7310~c;
  $$block7310~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == A)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block7310~b;
  $$block7310~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block7310~a;
  $$block7310~a: assume IsHeap($Heap); goto block7293;
  block7259: goto true7259to7310, false7259to7276;
  true7259to7310: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block7310;
  false7259to7276: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block7276;
  block7276: goto block7293;
  block7293: goto block7208;
  block7208: return;
  
}

axiom (AbstractCity0 <: AbstractCity0);
axiom ($BaseClass(AbstractCity0) == System.Object);
axiom ((AbstractCity0 <: $BaseClass(AbstractCity0)) && (AsDirectSubClass(AbstractCity0, $BaseClass(AbstractCity0)) == AbstractCity0));
axiom (!$IsImmutable(AbstractCity0) && ($AsMutable(AbstractCity0) == AbstractCity0));
axiom $IsMemberlessType(AbstractCity0);
axiom (forall $U : name :: {($U <: AbstractCity0)} (($U <: AbstractCity0) ==> ($U == AbstractCity0)));
axiom (B <: B);
axiom ($BaseClass(B) == System.Object);
axiom ((B <: $BaseClass(B)) && (AsDirectSubClass(B, $BaseClass(B)) == B));
axiom (!$IsImmutable(B) && ($AsMutable(B) == B));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: B)} (((IsHeap($h) && ($h[$oi, $inv] <: B)) && ($h[$oi, $localinv] != System.Object)) ==> (forall ^i : int :: (((0 <= ^i) && (^i <= ($Length($h[$oi, B.others]) - 1))) ==> (($IsNotNull(RefArrayGet($h[$h[$oi, B.others], $elements], ^i), AbstractCity0) && ($h[RefArrayGet($h[$h[$oi, B.others], $elements], ^i), AbstractCity0.a0] != null)) ==> ($h[$h[RefArrayGet($h[$h[$oi, B.others], $elements], ^i), AbstractCity0.a0], A.y] == 7))))));
procedure A.P(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation A.P(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, A); goto $$entry~j;
  $$entry~j: assume ($Heap[this, $allocated] == true); goto block8415;
  block8415: goto block8568;
  block8568: temp0 := this; goto $$block8568~j;
  $$block8568~j: havoc stack1s; goto $$block8568~i;
  $$block8568~i: assume $IsTokenForType(stack1s, A); goto $$block8568~h;
  $$block8568~h: stack1o := TypeObject(A); goto $$block8568~g;
  $$block8568~g: assert (temp0 != null); goto $$block8568~f;
  $$block8568~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: A)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block8568~e;
  $$block8568~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block8568~d;
  $$block8568~d: havoc temp1; goto $$block8568~c;
  $$block8568~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block8568~b;
  $$block8568~b: assume IsHeap($Heap); goto $$block8568~a;
  $$block8568~a: local2 := null; goto block8585;
  block8585: assert (this != null); goto $$block8585~i;
  $$block8585~i: local3 := $Heap[this, A.z]; goto $$block8585~h;
  $$block8585~h: stack0i := 1; goto $$block8585~g;
  $$block8585~g: stack0i := (local3 + stack0i); goto $$block8585~f;
  $$block8585~f: assert (this != null); goto $$block8585~e;
  $$block8585~e: assert (!($Heap[this, $inv] <: A) || ($Heap[this, $localinv] == System.Object)); goto $$block8585~d;
  $$block8585~d: assert (forall $o : ref, ^i : int :: (((0 <= ^i) && (^i <= ($Length($Heap[this, C.others]) - 1))) ==> ($IsNotNull(RefArrayGet($Heap[$Heap[this, C.others], $elements], ^i), AbstractCity1) ==> ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: C)) && ($Heap[RefArrayGet($Heap[$Heap[$o, C.others], $elements], ^i), AbstractCity1.a1] == this)) ==> (!($Heap[$o, $inv] <: C) || ($Heap[$o, $localinv] == System.Object)))))); goto $$block8585~c;
  $$block8585~c: $Heap := $Heap[this, A.z := stack0i]; goto $$block8585~b;
  $$block8585~b: assume IsHeap($Heap); goto $$block8585~a;
  $$block8585~a: stack0i := local3; goto block8670;
  block8670: stack0o := null; goto true8670to8738, false8670to8687;
  true8670to8738: assume (local2 == stack0o); goto block8738;
  false8670to8687: assume (local2 != stack0o); goto block8687;
  block8738: havoc stack0s; goto $$block8738~h;
  $$block8738~h: assume $IsTokenForType(stack0s, A); goto $$block8738~g;
  $$block8738~g: stack0o := TypeObject(A); goto $$block8738~f;
  $$block8738~f: assert (temp0 != null); goto $$block8738~e;
  $$block8738~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block8738~d;
  $$block8738~d: assert (forall ^ijk : int :: (((0 <= ^ijk) && (^ijk <= ($Length($Heap[temp0, A.others]) - 1))) ==> (((^ijk % 2) == 0) ==> ((RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk) != null) ==> ($Heap[RefArrayGet($Heap[$Heap[temp0, A.others], $elements], ^ijk), A.x] == 7))))); goto $$block8738~c;
  $$block8738~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == A)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block8738~b;
  $$block8738~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block8738~a;
  $$block8738~a: assume IsHeap($Heap); goto block8721;
  block8687: goto true8687to8738, false8687to8704;
  true8687to8738: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block8738;
  false8687to8704: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block8704;
  block8704: goto block8721;
  block8721: goto block8636;
  block8636: return;
  
}

axiom (AbstractCity1 <: AbstractCity1);
axiom ($BaseClass(AbstractCity1) == System.Object);
axiom ((AbstractCity1 <: $BaseClass(AbstractCity1)) && (AsDirectSubClass(AbstractCity1, $BaseClass(AbstractCity1)) == AbstractCity1));
axiom (!$IsImmutable(AbstractCity1) && ($AsMutable(AbstractCity1) == AbstractCity1));
axiom $IsMemberlessType(AbstractCity1);
axiom (forall $U : name :: {($U <: AbstractCity1)} (($U <: AbstractCity1) ==> ($U == AbstractCity1)));
axiom (C <: C);
axiom ($BaseClass(C) == System.Object);
axiom ((C <: $BaseClass(C)) && (AsDirectSubClass(C, $BaseClass(C)) == C));
axiom (!$IsImmutable(C) && ($AsMutable(C) == C));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: C)} (((IsHeap($h) && ($h[$oi, $inv] <: C)) && ($h[$oi, $localinv] != System.Object)) ==> (forall ^i : int :: (((0 <= ^i) && (^i <= ($Length($h[$oi, C.others]) - 1))) ==> ($IsNotNull(RefArrayGet($h[$h[$oi, C.others], $elements], ^i), AbstractCity1) ==> (($h[RefArrayGet($h[$h[$oi, C.others], $elements], ^i), AbstractCity1.a1] != null) ==> ($h[$h[RefArrayGet($h[$h[$oi, C.others], $elements], ^i), AbstractCity1.a1], A.z] == 7)))))));
procedure A..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation A..cctor() {
  entry: goto block9554;
  block9554: goto block9605;
  block9605: return;
  
}

procedure B.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation B.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var local0 : bool where true;
  var local1 : int where InRange(local1, System.Int32);
  var stack0o : ref;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local2 : bool where true;
  var stack1o : ref;
  var SS$Display.Return.Local : bool where true;
  var stack50000o : ref;
  var $Heap$block10166$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, B); goto $$entry~l;
  $$entry~l: assume ($Heap[this, $allocated] == true); goto $$entry~k;
  $$entry~k: throwException := throwException$in; goto block10132;
  block10132: goto block10149;
  block10149: local0 := true; goto $$block10149~a;
  $$block10149~a: local1 := 0; goto block10166$LoopPreheader;
  block10166: assume (((forall $o : ref :: (($Heap$block10166$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block10166$LoopPreheader[$ot, $allocated] == true) && ($Heap$block10166$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block10166$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block10166$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block10166$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block10166~i;
  $$block10166~i: assume (forall $o : ref :: ((($Heap$block10166$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block10166$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block10166$LoopPreheader[$o, $allocated] != true))); goto $$block10166~h;
  $$block10166~h: assume (forall $o : ref :: ((($Heap$block10166$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block10166~g;
  $$block10166~g: assert (forall $o : ref :: ((($o != null) && ($Heap$block10166$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block10166$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block10166$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block10166~f;
  $$block10166~f: assert (this != null); goto $$block10166~e;
  $$block10166~e: stack0o := $Heap[this, B.others]; goto $$block10166~d;
  $$block10166~d: assert (stack0o != null); goto $$block10166~c;
  $$block10166~c: stack0i := $Length(stack0o); goto $$block10166~b;
  $$block10166~b: stack1i := 1; goto $$block10166~a;
  $$block10166~a: stack0i := (stack0i - stack1i); goto true10166to10353, false10166to10183;
  true10166to10353: assume (local1 > stack0i); goto block10353;
  false10166to10183: assume (local1 <= stack0i); goto block10183;
  block10353: goto true10353to10455, false10353to10370;
  block10183: assert (this != null); goto $$block10183~g;
  $$block10183~g: stack0o := $Heap[this, B.others]; goto $$block10183~f;
  $$block10183~f: stack1i := local1; goto $$block10183~e;
  $$block10183~e: assert (stack0o != null); goto $$block10183~d;
  $$block10183~d: assert (0 <= stack1i); goto $$block10183~c;
  $$block10183~c: assert (stack1i < $Length(stack0o)); goto $$block10183~b;
  $$block10183~b: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block10183~a;
  $$block10183~a: stack0o := $As(stack0o, AbstractCity0); goto true10183to10285, false10183to10200;
  true10353to10455: assume local0; goto block10455;
  false10353to10370: assume !local0; goto block10370;
  block10455: local2 := true; goto block10472;
  block10370: stack0b := throwException; goto true10370to10421, false10370to10387;
  true10183to10285: assume (stack0o == null); goto block10285;
  false10183to10200: assume (stack0o != null); goto block10200;
  block10285: stack0b := true; goto block10302;
  block10200: assert (this != null); goto $$block10200~k;
  $$block10200~k: stack0o := $Heap[this, B.others]; goto $$block10200~j;
  $$block10200~j: stack1i := local1; goto $$block10200~i;
  $$block10200~i: assert (stack0o != null); goto $$block10200~h;
  $$block10200~h: assert (0 <= stack1i); goto $$block10200~g;
  $$block10200~g: assert (stack1i < $Length(stack0o)); goto $$block10200~f;
  $$block10200~f: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block10200~e;
  $$block10200~e: assert $Is(stack0o, AbstractCity0); goto $$block10200~d;
  $$block10200~d: stack0o := stack0o; goto $$block10200~c;
  $$block10200~c: assert (stack0o != null); goto $$block10200~b;
  $$block10200~b: stack0o := $Heap[stack0o, AbstractCity0.a0]; goto $$block10200~a;
  $$block10200~a: stack1o := null; goto true10200to10285, false10200to10217;
  true10370to10421: assume !stack0b; goto block10421;
  false10370to10387: assume stack0b; goto block10387;
  block10421: local2 := false; goto block10472;
  block10387: assume false; goto $$block10387~i;
  $$block10387~i: havoc stack50000o; goto $$block10387~h;
  $$block10387~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block10387~g;
  $$block10387~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block10387~f;
  $$block10387~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block10387~e;
  $$block10387~e: assert (stack50000o != null); goto $$block10387~d;
  $$block10387~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block10387~c;
  $$block10387~c: stack0o := stack50000o; goto $$block10387~b;
  $$block10387~b: assert (stack0o != null); goto $$block10387~a;
  $$block10387~a: assume false; return;
  true10200to10285: assume (stack0o == stack1o); goto block10285;
  false10200to10217: assume (stack0o != stack1o); goto block10217;
  block10217: assert (this != null); goto $$block10217~m;
  $$block10217~m: stack0o := $Heap[this, B.others]; goto $$block10217~l;
  $$block10217~l: stack1i := local1; goto $$block10217~k;
  $$block10217~k: assert (stack0o != null); goto $$block10217~j;
  $$block10217~j: assert (0 <= stack1i); goto $$block10217~i;
  $$block10217~i: assert (stack1i < $Length(stack0o)); goto $$block10217~h;
  $$block10217~h: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block10217~g;
  $$block10217~g: assert $Is(stack0o, AbstractCity0); goto $$block10217~f;
  $$block10217~f: stack0o := stack0o; goto $$block10217~e;
  $$block10217~e: assert (stack0o != null); goto $$block10217~d;
  $$block10217~d: stack0o := $Heap[stack0o, AbstractCity0.a0]; goto $$block10217~c;
  $$block10217~c: assert (stack0o != null); goto $$block10217~b;
  $$block10217~b: stack0i := $Heap[stack0o, A.y]; goto $$block10217~a;
  $$block10217~a: stack1i := 7; goto true10217to10251, false10217to10234;
  block10472: SS$Display.Return.Local := local2; goto $$block10472~b;
  $$block10472~b: stack0b := local2; goto $$block10472~a;
  $$block10472~a: $result := stack0b; return;
  true10217to10251: assume (stack0i == stack1i); goto block10251;
  false10217to10234: assume (stack0i != stack1i); goto block10234;
  block10251: stack0b := true; goto block10268;
  block10234: stack0b := false; goto block10268;
  block10302: local0 := stack0b; goto true10302to10336, false10302to10319;
  true10302to10336: assume local0; goto block10336;
  false10302to10319: assume !local0; goto block10319;
  block10336: stack0i := 1; goto $$block10336~b;
  $$block10336~b: stack0i := (local1 + stack0i); goto $$block10336~a;
  $$block10336~a: local1 := stack0i; goto block10166;
  block10319: goto block10353;
  block10268: goto block10302;
  block10166$LoopPreheader: $Heap$block10166$LoopPreheader := $Heap; goto block10166;
  
}

procedure B..ctor$System.Int32(this : ref, n$in : int where InRange(n$in, System.Int32));
  free requires true;
  requires (0 <= n$in);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == B)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(B <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation B..ctor$System.Int32(this : ref, n$in : int) {
  var n : int where InRange(n, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var temp0 : ref;
  entry: assume $IsNotNull(this, B); goto $$entry~o;
  $$entry~o: assume ($Heap[this, $allocated] == true); goto $$entry~n;
  $$entry~n: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~m;
  $$entry~m: n := n$in; goto block11747;
  block11747: goto block11849;
  block11849: assert (this != null); goto $$block11849~a;
  $$block11849~a: call System.Object..ctor(this); goto block11917;
  block11917: stack0i := n; goto $$block11917~v;
  $$block11917~v: assert (0 <= stack0i); goto $$block11917~u;
  $$block11917~u: havoc stack0o; goto $$block11917~t;
  $$block11917~t: assume (($Heap[stack0o, $allocated] == false) && ($Length(stack0o) == stack0i)); goto $$block11917~s;
  $$block11917~s: assume $IsNotNull(stack0o, RefArray(AbstractCity0, 1)); goto $$block11917~r;
  $$block11917~r: assume (($Heap[stack0o, $ownerRef] == stack0o) && ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block11917~q;
  $$block11917~q: assume ((($Heap[stack0o, $inv] == RefArray(AbstractCity0, 1)) && ($Heap[stack0o, $localinv] == RefArray(AbstractCity0, 1))) && ((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame])))); goto $$block11917~p;
  $$block11917~p: assume (forall $i : int :: (RefArrayGet($Heap[stack0o, $elements], $i) == null)); goto $$block11917~o;
  $$block11917~o: $Heap := $Heap[stack0o, $allocated := true]; goto $$block11917~n;
  $$block11917~n: assume IsHeap($Heap); goto $$block11917~m;
  $$block11917~m: assert (this != null); goto $$block11917~l;
  $$block11917~l: assert (!($Heap[this, $inv] <: B) || ($Heap[this, $localinv] == System.Object)); goto $$block11917~k;
  $$block11917~k: assert (($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || (($Heap[stack0o, $ownerRef] == this) && ($Heap[stack0o, $ownerFrame] == B))); goto $$block11917~j;
  $$block11917~j: $Heap := $Heap[this, B.others := stack0o]; goto $$block11917~i;
  $$block11917~i: call $UpdateOwnersForRep(this, B, stack0o); goto $$block11917~h;
  $$block11917~h: assume IsHeap($Heap); goto $$block11917~g;
  $$block11917~g: temp0 := this; goto $$block11917~f;
  $$block11917~f: assert (temp0 != null); goto $$block11917~e;
  $$block11917~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11917~d;
  $$block11917~d: assert (forall ^i : int :: (((0 <= ^i) && (^i <= ($Length($Heap[temp0, B.others]) - 1))) ==> (($IsNotNull(RefArrayGet($Heap[$Heap[temp0, B.others], $elements], ^i), AbstractCity0) && ($Heap[RefArrayGet($Heap[$Heap[temp0, B.others], $elements], ^i), AbstractCity0.a0] != null)) ==> ($Heap[$Heap[RefArrayGet($Heap[$Heap[temp0, B.others], $elements], ^i), AbstractCity0.a0], A.y] == 7)))); goto $$block11917~c;
  $$block11917~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == B)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11917~b;
  $$block11917~b: $Heap := $Heap[temp0, $inv := B]; goto $$block11917~a;
  $$block11917~a: assume IsHeap($Heap); return;
  
}

procedure B..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation B..cctor() {
  entry: goto block12308;
  block12308: goto block12359;
  block12359: return;
  
}

procedure C.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var local0 : bool where true;
  var local1 : int where InRange(local1, System.Int32);
  var stack0o : ref;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var stack1o : ref;
  var local2 : bool where true;
  var stack50000o : ref;
  var SS$Display.Return.Local : bool where true;
  var $Heap$block12937$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, C); goto $$entry~q;
  $$entry~q: assume ($Heap[this, $allocated] == true); goto $$entry~p;
  $$entry~p: throwException := throwException$in; goto block12903;
  block12903: goto block12920;
  block12920: local0 := true; goto $$block12920~a;
  $$block12920~a: local1 := 0; goto block12937$LoopPreheader;
  block12937: assume (((forall $o : ref :: (($Heap$block12937$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block12937$LoopPreheader[$ot, $allocated] == true) && ($Heap$block12937$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block12937$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block12937$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block12937$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block12937~i;
  $$block12937~i: assume (forall $o : ref :: ((($Heap$block12937$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block12937$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block12937$LoopPreheader[$o, $allocated] != true))); goto $$block12937~h;
  $$block12937~h: assume (forall $o : ref :: ((($Heap$block12937$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block12937~g;
  $$block12937~g: assert (forall $o : ref :: ((($o != null) && ($Heap$block12937$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block12937$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block12937$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block12937~f;
  $$block12937~f: assert (this != null); goto $$block12937~e;
  $$block12937~e: stack0o := $Heap[this, C.others]; goto $$block12937~d;
  $$block12937~d: assert (stack0o != null); goto $$block12937~c;
  $$block12937~c: stack0i := $Length(stack0o); goto $$block12937~b;
  $$block12937~b: stack1i := 1; goto $$block12937~a;
  $$block12937~a: stack0i := (stack0i - stack1i); goto true12937to13141, false12937to12954;
  true12937to13141: assume (local1 > stack0i); goto block13141;
  false12937to12954: assume (local1 <= stack0i); goto block12954;
  block13141: goto true13141to13243, false13141to13158;
  block12954: assert (this != null); goto $$block12954~g;
  $$block12954~g: stack0o := $Heap[this, C.others]; goto $$block12954~f;
  $$block12954~f: stack1i := local1; goto $$block12954~e;
  $$block12954~e: assert (stack0o != null); goto $$block12954~d;
  $$block12954~d: assert (0 <= stack1i); goto $$block12954~c;
  $$block12954~c: assert (stack1i < $Length(stack0o)); goto $$block12954~b;
  $$block12954~b: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block12954~a;
  $$block12954~a: stack0o := $As(stack0o, AbstractCity1); goto true12954to13090, false12954to12971;
  true12954to13090: assume (stack0o == null); goto block13090;
  false12954to12971: assume (stack0o != null); goto block12971;
  block13090: goto true13090to13124, false13090to13107;
  block12971: assert (this != null); goto $$block12971~k;
  $$block12971~k: stack0o := $Heap[this, C.others]; goto $$block12971~j;
  $$block12971~j: stack1i := local1; goto $$block12971~i;
  $$block12971~i: assert (stack0o != null); goto $$block12971~h;
  $$block12971~h: assert (0 <= stack1i); goto $$block12971~g;
  $$block12971~g: assert (stack1i < $Length(stack0o)); goto $$block12971~f;
  $$block12971~f: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block12971~e;
  $$block12971~e: assert $Is(stack0o, AbstractCity1); goto $$block12971~d;
  $$block12971~d: stack0o := stack0o; goto $$block12971~c;
  $$block12971~c: assert (stack0o != null); goto $$block12971~b;
  $$block12971~b: stack0o := $Heap[stack0o, AbstractCity1.a1]; goto $$block12971~a;
  $$block12971~a: stack1o := null; goto true12971to13056, false12971to12988;
  true13141to13243: assume local0; goto block13243;
  false13141to13158: assume !local0; goto block13158;
  block13243: local2 := true; goto block13260;
  block13158: stack0b := throwException; goto true13158to13209, false13158to13175;
  true13090to13124: assume local0; goto block13124;
  false13090to13107: assume !local0; goto block13107;
  block13124: stack0i := 1; goto $$block13124~b;
  $$block13124~b: stack0i := (local1 + stack0i); goto $$block13124~a;
  $$block13124~a: local1 := stack0i; goto block12937;
  block13107: goto block13141;
  true12971to13056: assume (stack0o == stack1o); goto block13056;
  false12971to12988: assume (stack0o != stack1o); goto block12988;
  block13056: stack0b := true; goto block13073;
  block12988: assert (this != null); goto $$block12988~m;
  $$block12988~m: stack0o := $Heap[this, C.others]; goto $$block12988~l;
  $$block12988~l: stack1i := local1; goto $$block12988~k;
  $$block12988~k: assert (stack0o != null); goto $$block12988~j;
  $$block12988~j: assert (0 <= stack1i); goto $$block12988~i;
  $$block12988~i: assert (stack1i < $Length(stack0o)); goto $$block12988~h;
  $$block12988~h: stack0o := RefArrayGet($Heap[stack0o, $elements], stack1i); goto $$block12988~g;
  $$block12988~g: assert $Is(stack0o, AbstractCity1); goto $$block12988~f;
  $$block12988~f: stack0o := stack0o; goto $$block12988~e;
  $$block12988~e: assert (stack0o != null); goto $$block12988~d;
  $$block12988~d: stack0o := $Heap[stack0o, AbstractCity1.a1]; goto $$block12988~c;
  $$block12988~c: assert (stack0o != null); goto $$block12988~b;
  $$block12988~b: stack0i := $Heap[stack0o, A.z]; goto $$block12988~a;
  $$block12988~a: stack1i := 7; goto true12988to13022, false12988to13005;
  true13158to13209: assume !stack0b; goto block13209;
  false13158to13175: assume stack0b; goto block13175;
  block13209: local2 := false; goto block13260;
  block13175: assume false; goto $$block13175~i;
  $$block13175~i: havoc stack50000o; goto $$block13175~h;
  $$block13175~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block13175~g;
  $$block13175~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block13175~f;
  $$block13175~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block13175~e;
  $$block13175~e: assert (stack50000o != null); goto $$block13175~d;
  $$block13175~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block13175~c;
  $$block13175~c: stack0o := stack50000o; goto $$block13175~b;
  $$block13175~b: assert (stack0o != null); goto $$block13175~a;
  $$block13175~a: assume false; return;
  true12988to13022: assume (stack0i == stack1i); goto block13022;
  false12988to13005: assume (stack0i != stack1i); goto block13005;
  block13022: stack0b := true; goto block13039;
  block13005: stack0b := false; goto block13039;
  block13260: SS$Display.Return.Local := local2; goto $$block13260~b;
  $$block13260~b: stack0b := local2; goto $$block13260~a;
  $$block13260~a: $result := stack0b; return;
  block13073: local0 := stack0b; goto block13090;
  block13039: goto block13073;
  block12937$LoopPreheader: $Heap$block12937$LoopPreheader := $Heap; goto block12937;
  
}

procedure C..ctor$System.Int32(this : ref, n$in : int where InRange(n$in, System.Int32));
  free requires true;
  requires (0 <= n$in);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == C)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(C <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation C..ctor$System.Int32(this : ref, n$in : int) {
  var n : int where InRange(n, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var temp0 : ref;
  entry: assume $IsNotNull(this, C); goto $$entry~t;
  $$entry~t: assume ($Heap[this, $allocated] == true); goto $$entry~s;
  $$entry~s: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~r;
  $$entry~r: n := n$in; goto block14535;
  block14535: goto block14637;
  block14637: assert (this != null); goto $$block14637~a;
  $$block14637~a: call System.Object..ctor(this); goto block14705;
  block14705: stack0i := n; goto $$block14705~v;
  $$block14705~v: assert (0 <= stack0i); goto $$block14705~u;
  $$block14705~u: havoc stack0o; goto $$block14705~t;
  $$block14705~t: assume (($Heap[stack0o, $allocated] == false) && ($Length(stack0o) == stack0i)); goto $$block14705~s;
  $$block14705~s: assume $IsNotNull(stack0o, RefArray(AbstractCity1, 1)); goto $$block14705~r;
  $$block14705~r: assume (($Heap[stack0o, $ownerRef] == stack0o) && ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block14705~q;
  $$block14705~q: assume ((($Heap[stack0o, $inv] == RefArray(AbstractCity1, 1)) && ($Heap[stack0o, $localinv] == RefArray(AbstractCity1, 1))) && ((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame])))); goto $$block14705~p;
  $$block14705~p: assume (forall $i : int :: (RefArrayGet($Heap[stack0o, $elements], $i) == null)); goto $$block14705~o;
  $$block14705~o: $Heap := $Heap[stack0o, $allocated := true]; goto $$block14705~n;
  $$block14705~n: assume IsHeap($Heap); goto $$block14705~m;
  $$block14705~m: assert (this != null); goto $$block14705~l;
  $$block14705~l: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block14705~k;
  $$block14705~k: assert (($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || (($Heap[stack0o, $ownerRef] == this) && ($Heap[stack0o, $ownerFrame] == C))); goto $$block14705~j;
  $$block14705~j: $Heap := $Heap[this, C.others := stack0o]; goto $$block14705~i;
  $$block14705~i: call $UpdateOwnersForRep(this, C, stack0o); goto $$block14705~h;
  $$block14705~h: assume IsHeap($Heap); goto $$block14705~g;
  $$block14705~g: temp0 := this; goto $$block14705~f;
  $$block14705~f: assert (temp0 != null); goto $$block14705~e;
  $$block14705~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block14705~d;
  $$block14705~d: assert (forall ^i : int :: (((0 <= ^i) && (^i <= ($Length($Heap[temp0, C.others]) - 1))) ==> ($IsNotNull(RefArrayGet($Heap[$Heap[temp0, C.others], $elements], ^i), AbstractCity1) ==> (($Heap[RefArrayGet($Heap[$Heap[temp0, C.others], $elements], ^i), AbstractCity1.a1] != null) ==> ($Heap[$Heap[RefArrayGet($Heap[$Heap[temp0, C.others], $elements], ^i), AbstractCity1.a1], A.z] == 7))))); goto $$block14705~c;
  $$block14705~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14705~b;
  $$block14705~b: $Heap := $Heap[temp0, $inv := C]; goto $$block14705~a;
  $$block14705~a: assume IsHeap($Heap); return;
  
}

procedure C..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C..cctor() {
  entry: goto block15096;
  block15096: goto block15147;
  block15147: return;
  
}

procedure AbstractCity0..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == AbstractCity0)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(AbstractCity0 <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation AbstractCity0..ctor(this : ref) {
  entry: assume $IsNotNull(this, AbstractCity0); goto $$entry~w;
  $$entry~w: assume ($Heap[this, $allocated] == true); goto $$entry~v;
  $$entry~v: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~u;
  $$entry~u: assume ($Heap[this, AbstractCity0.a0] == null); goto block15351;
  block15351: goto block15368;
  block15368: assert (this != null); goto $$block15368~f;
  $$block15368~f: call System.Object..ctor(this); goto $$block15368~e;
  $$block15368~e: assert (this != null); goto $$block15368~d;
  $$block15368~d: assert (($Heap[this, $inv] == System.Object) && ($Heap[this, $localinv] == $typeof(this))); goto $$block15368~c;
  $$block15368~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == this)) && ($Heap[$p, $ownerFrame] == AbstractCity0)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block15368~b;
  $$block15368~b: $Heap := $Heap[this, $inv := AbstractCity0]; goto $$block15368~a;
  $$block15368~a: assume IsHeap($Heap); return;
  
}

procedure AbstractCity1..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == AbstractCity1)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(AbstractCity1 <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation AbstractCity1..ctor(this : ref) {
  entry: assume $IsNotNull(this, AbstractCity1); goto $$entry~z;
  $$entry~z: assume ($Heap[this, $allocated] == true); goto $$entry~y;
  $$entry~y: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~x;
  $$entry~x: assume ($Heap[this, AbstractCity1.a1] == null); goto block15538;
  block15538: goto block15555;
  block15555: assert (this != null); goto $$block15555~f;
  $$block15555~f: call System.Object..ctor(this); goto $$block15555~e;
  $$block15555~e: assert (this != null); goto $$block15555~d;
  $$block15555~d: assert (($Heap[this, $inv] == System.Object) && ($Heap[this, $localinv] == $typeof(this))); goto $$block15555~c;
  $$block15555~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == this)) && ($Heap[$p, $ownerFrame] == AbstractCity1)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block15555~b;
  $$block15555~b: $Heap := $Heap[this, $inv := AbstractCity1]; goto $$block15555~a;
  $$block15555~a: assume IsHeap($Heap); return;
  
}

axiom (AnotherInvariantNameIssue <: AnotherInvariantNameIssue);
axiom ($BaseClass(AnotherInvariantNameIssue) == System.Object);
axiom ((AnotherInvariantNameIssue <: $BaseClass(AnotherInvariantNameIssue)) && (AsDirectSubClass(AnotherInvariantNameIssue, $BaseClass(AnotherInvariantNameIssue)) == AnotherInvariantNameIssue));
axiom (!$IsImmutable(AnotherInvariantNameIssue) && ($AsMutable(AnotherInvariantNameIssue) == AnotherInvariantNameIssue));
axiom (forall $U : name :: {($U <: AnotherInvariantNameIssue)} (($U <: AnotherInvariantNameIssue) ==> ($U == AnotherInvariantNameIssue)));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: AnotherInvariantNameIssue)} (((IsHeap($h) && ($h[$oi, $inv] <: AnotherInvariantNameIssue)) && ($h[$oi, $localinv] != System.Object)) ==> (forall ^j : int, ^i : int :: (((0 <= ^i) && (^i <= ($h[$oi, AnotherInvariantNameIssue.x] - 1))) ==> (((^i % 2) == 0) ==> (((^i <= ^j) && (^j <= ((2 * $h[$oi, AnotherInvariantNameIssue.x]) - 1))) ==> (((^i + ^j) < 200) ==> (^i < $h[$oi, AnotherInvariantNameIssue.x]))))))));
procedure AnotherInvariantNameIssue.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation AnotherInvariantNameIssue.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var local0 : bool where true;
  var local1 : int where InRange(local1, System.Int32);
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local3 : bool where true;
  var local2 : int where InRange(local2, System.Int32);
  var SS$Display.Return.Local : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var $Heap$block16150$LoopPreheader : <x>[ref, name]x;
  var $Heap$block16201$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, AnotherInvariantNameIssue); goto $$entry~ab;
  $$entry~ab: assume ($Heap[this, $allocated] == true); goto $$entry~aa;
  $$entry~aa: throwException := throwException$in; goto block16116;
  block16116: goto block16133;
  block16133: local0 := true; goto $$block16133~a;
  $$block16133~a: local1 := 0; goto block16150$LoopPreheader;
  block16150: assume (((forall $o : ref :: (($Heap$block16150$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block16150$LoopPreheader[$ot, $allocated] == true) && ($Heap$block16150$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block16150$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block16150$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block16150$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block16150~g;
  $$block16150~g: assume (forall $o : ref :: ((($Heap$block16150$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block16150$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block16150$LoopPreheader[$o, $allocated] != true))); goto $$block16150~f;
  $$block16150~f: assume (forall $o : ref :: ((($Heap$block16150$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block16150~e;
  $$block16150~e: assert (forall $o : ref :: ((($o != null) && ($Heap$block16150$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block16150$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block16150$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block16150~d;
  $$block16150~d: assert (this != null); goto $$block16150~c;
  $$block16150~c: stack0i := $Heap[this, AnotherInvariantNameIssue.x]; goto $$block16150~b;
  $$block16150~b: stack1i := 1; goto $$block16150~a;
  $$block16150~a: stack0i := (stack0i - stack1i); goto true16150to16405, false16150to16167;
  true16150to16405: assume (local1 > stack0i); goto block16405;
  false16150to16167: assume (local1 <= stack0i); goto block16167;
  block16405: goto true16405to16507, false16405to16422;
  block16167: stack0i := 2; goto $$block16167~c;
  $$block16167~c: assert (stack0i != 0); goto $$block16167~b;
  $$block16167~b: stack0i := (local1 % stack0i); goto $$block16167~a;
  $$block16167~a: stack1i := 0; goto true16167to16354, false16167to16184;
  true16405to16507: assume local0; goto block16507;
  false16405to16422: assume !local0; goto block16422;
  block16507: local3 := true; goto block16524;
  block16422: stack0b := throwException; goto true16422to16473, false16422to16439;
  true16167to16354: assume (stack0i != stack1i); goto block16354;
  false16167to16184: assume (stack0i == stack1i); goto block16184;
  block16354: goto true16354to16388, false16354to16371;
  block16184: local2 := local1; goto block16201$LoopPreheader;
  true16422to16473: assume !stack0b; goto block16473;
  false16422to16439: assume stack0b; goto block16439;
  block16473: local3 := false; goto block16524;
  block16439: assume false; goto $$block16439~i;
  $$block16439~i: havoc stack50000o; goto $$block16439~h;
  $$block16439~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block16439~g;
  $$block16439~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block16439~f;
  $$block16439~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block16439~e;
  $$block16439~e: assert (stack50000o != null); goto $$block16439~d;
  $$block16439~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block16439~c;
  $$block16439~c: stack0o := stack50000o; goto $$block16439~b;
  $$block16439~b: assert (stack0o != null); goto $$block16439~a;
  $$block16439~a: assume false; return;
  true16354to16388: assume local0; goto block16388;
  false16354to16371: assume !local0; goto block16371;
  block16388: stack0i := 1; goto $$block16388~b;
  $$block16388~b: stack0i := (local1 + stack0i); goto $$block16388~a;
  $$block16388~a: local1 := stack0i; goto block16150;
  block16371: goto block16405;
  block16524: SS$Display.Return.Local := local3; goto $$block16524~b;
  $$block16524~b: stack0b := local3; goto $$block16524~a;
  $$block16524~a: $result := stack0b; return;
  block16201: assume (((forall $o : ref :: (($Heap$block16201$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block16201$LoopPreheader[$ot, $allocated] == true) && ($Heap$block16201$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block16201$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block16201$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block16201$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block16201~i;
  $$block16201~i: assume (forall $o : ref :: ((($Heap$block16201$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block16201$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block16201$LoopPreheader[$o, $allocated] != true))); goto $$block16201~h;
  $$block16201~h: assume (forall $o : ref :: ((($Heap$block16201$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block16201~g;
  $$block16201~g: assert (forall $o : ref :: ((($o != null) && ($Heap$block16201$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block16201$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block16201$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block16201~f;
  $$block16201~f: stack0i := 2; goto $$block16201~e;
  $$block16201~e: assert (this != null); goto $$block16201~d;
  $$block16201~d: stack1i := $Heap[this, AnotherInvariantNameIssue.x]; goto $$block16201~c;
  $$block16201~c: stack0i := (stack0i * stack1i); goto $$block16201~b;
  $$block16201~b: stack1i := 1; goto $$block16201~a;
  $$block16201~a: stack0i := (stack0i - stack1i); goto true16201to16354, false16201to16218;
  true16201to16354: assume (local2 > stack0i); goto block16354;
  false16201to16218: assume (local2 <= stack0i); goto block16218;
  block16218: stack0i := (local1 + local2); goto $$block16218~a;
  $$block16218~a: stack1i := 200; goto true16218to16303, false16218to16235;
  true16218to16303: assume (stack0i >= stack1i); goto block16303;
  false16218to16235: assume (stack0i < stack1i); goto block16235;
  block16303: goto true16303to16337, false16303to16320;
  block16235: assert (this != null); goto $$block16235~a;
  $$block16235~a: stack0i := $Heap[this, AnotherInvariantNameIssue.x]; goto true16235to16269, false16235to16252;
  true16303to16337: assume local0; goto block16337;
  false16303to16320: assume !local0; goto block16320;
  block16337: stack0i := 1; goto $$block16337~b;
  $$block16337~b: stack0i := (local2 + stack0i); goto $$block16337~a;
  $$block16337~a: local2 := stack0i; goto block16201;
  block16320: goto block16354;
  true16235to16269: assume (local1 < stack0i); goto block16269;
  false16235to16252: assume (local1 >= stack0i); goto block16252;
  block16269: stack0b := true; goto block16286;
  block16252: stack0b := false; goto block16286;
  block16286: local0 := stack0b; goto block16303;
  block16150$LoopPreheader: $Heap$block16150$LoopPreheader := $Heap; goto block16150;
  block16201$LoopPreheader: $Heap$block16201$LoopPreheader := $Heap; goto block16201;
  
}

procedure AnotherInvariantNameIssue..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == AnotherInvariantNameIssue)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(AnotherInvariantNameIssue <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation AnotherInvariantNameIssue..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, AnotherInvariantNameIssue); goto $$entry~ae;
  $$entry~ae: assume ($Heap[this, $allocated] == true); goto $$entry~ad;
  $$entry~ad: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~ac;
  $$entry~ac: assume ($Heap[this, AnotherInvariantNameIssue.x] == 0); goto block17680;
  block17680: goto block17697;
  block17697: assert (this != null); goto $$block17697~a;
  $$block17697~a: call System.Object..ctor(this); goto block17765;
  block17765: temp0 := this; goto $$block17765~f;
  $$block17765~f: assert (temp0 != null); goto $$block17765~e;
  $$block17765~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block17765~d;
  $$block17765~d: assert (forall ^j : int, ^i : int :: (((0 <= ^i) && (^i <= ($Heap[temp0, AnotherInvariantNameIssue.x] - 1))) ==> (((^i % 2) == 0) ==> (((^i <= ^j) && (^j <= ((2 * $Heap[temp0, AnotherInvariantNameIssue.x]) - 1))) ==> (((^i + ^j) < 200) ==> (^i < $Heap[temp0, AnotherInvariantNameIssue.x])))))); goto $$block17765~c;
  $$block17765~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == AnotherInvariantNameIssue)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block17765~b;
  $$block17765~b: $Heap := $Heap[temp0, $inv := AnotherInvariantNameIssue]; goto $$block17765~a;
  $$block17765~a: assume IsHeap($Heap); return;
  
}

procedure AnotherInvariantNameIssue..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation AnotherInvariantNameIssue..cctor() {
  entry: goto block18054;
  block18054: goto block18105;
  block18105: return;
  
}

